Inference at * 1 
Iof proof for Lemma dcdr-to-bool-equivalence:



1. P : 
2. d : Dec(P)
3. [d]
  P 

latex

 by Unfold `decidable` ( 2) 

latex

 1: 

 1: 2. d : P  (P)
 1: 3. [d]
 1:   P
 .

Definitions

Dec(P)